<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>LogicalSystem</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="LogicalSystem";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/lang/LogHyp.html" title="class in mmj.lang"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/lang/LogicFormula.html" title="class in mmj.lang"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/lang/LogicalSystem.html" target="_top">Frames</a></li>
<li><a href="LogicalSystem.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.lang</div>
<h2 title="Class LogicalSystem" class="title">Class LogicalSystem</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li>mmj.lang.LogicalSystem</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<dl>
<dt>All Implemented Interfaces:</dt>
<dd><a href="../../mmj/lang/SystemLoader.html" title="interface in mmj.lang">SystemLoader</a></dd>
</dl>
<hr>
<br>
<pre>public class <span class="strong">LogicalSystem</span>
extends java.lang.Object
implements <a href="../../mmj/lang/SystemLoader.html" title="interface in mmj.lang">SystemLoader</a></pre>
<div class="block">The <code>LogicalSystem</code>, along with the rest of the <code>mmj.lang</code>
 package, implements the abstract portion of the Metamath language -- the
 "object" language of Metamath, as opposed to the "metalanguage" of Metamath
 source files. For example, note that <code>LogicalSystem.java</code> does not care
 which characters are used in Constant, Variable and Label strings. The
 characters are represented internally in Unicode, not the 7-bit ASCII
 employed in Metamath (.mm) source files. Nevertheless, the logical rules
 concerning Constant, Variable and Label <i>namespaces</i> are enforced
 rigorously :) As much as possible, the concerns of source files are delegated
 to the <code>mmj.mmio</code> package and its highest level class,
 <code>Systemizer.java</code>, which uses <code>LogicalSystem.java</code> to create a
 Metamath logical system in memory. Once <code>Systemizer.java</code> has input a
 set of Metamath statements into a <code>LogicalSystem.java</code> object, the
 Logical System can be processed independently of all <code>mmj.mmio</code> code.
 In fact, a GUI system need not use <code>mmj.mmio</code> or
 <code>Systemizer.java</code> at all (however it should be noted that none of this
 code is "thread aware" as of now...)</div>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../MetamathERNotes.html"> Nomenclature and
      Entity-Relationship Notes</a></dd></dl>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colOne" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/lang/LogicalSystem.html#LogicalSystem(java.lang.String, java.lang.String, mmj.gmff.GMFFManager, mmj.lang.BookManager, mmj.lang.SeqAssigner, int, int, mmj.lang.ProofVerifier, mmj.lang.SyntaxVerifier)">LogicalSystem</a></strong>(java.lang.String&nbsp;provableLogicStmtTypeParm,
             java.lang.String&nbsp;logicStmtTypeParm,
             <a href="../../mmj/gmff/GMFFManager.html" title="class in mmj.gmff">GMFFManager</a>&nbsp;gmffManager,
             <a href="../../mmj/lang/BookManager.html" title="class in mmj.lang">BookManager</a>&nbsp;bookManager,
             <a href="../../mmj/lang/SeqAssigner.html" title="class in mmj.lang">SeqAssigner</a>&nbsp;seqAssigner,
             int&nbsp;symTblInitialSize,
             int&nbsp;stmtTblInitialSize,
             <a href="../../mmj/lang/ProofVerifier.html" title="interface in mmj.lang">ProofVerifier</a>&nbsp;proofVerifier,
             <a href="../../mmj/lang/SyntaxVerifier.html" title="interface in mmj.lang">SyntaxVerifier</a>&nbsp;syntaxVerifier)</code>
<div class="block">Construct with full set of parameters.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#accumTheoremLoaderCommitListener(mmj.tl.TheoremLoaderCommitListener)">accumTheoremLoaderCommitListener</a></strong>(<a href="../../mmj/tl/TheoremLoaderCommitListener.html" title="interface in mmj.tl">TheoremLoaderCommitListener</a>&nbsp;t)</code>
<div class="block">Adds a TheoremLoaderCommitListener to the TheoremLoaderCommitListener
 list if the instance is not already in the list.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/Axiom.html" title="class in mmj.lang">Axiom</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#addAxiom(java.lang.String, java.lang.String, java.util.List)">addAxiom</a></strong>(java.lang.String&nbsp;labelS,
        java.lang.String&nbsp;typS,
        java.util.List&lt;java.lang.String&gt;&nbsp;symList)</code>
<div class="block">Add Axiom to Logical System.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#addCnst(java.lang.String)">addCnst</a></strong>(java.lang.String&nbsp;id)</code>
<div class="block">Add Cnst to Logical System.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#addDjVars(java.lang.String, java.lang.String)">addDjVars</a></strong>(java.lang.String&nbsp;djVar1S,
         java.lang.String&nbsp;djVar2S)</code>
<div class="block">Add DjVars (Disjoint Variables Restriction) to Logical System.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/LogHyp.html" title="class in mmj.lang">LogHyp</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#addLogHyp(java.lang.String, java.lang.String, java.util.List)">addLogHyp</a></strong>(java.lang.String&nbsp;labelS,
         java.lang.String&nbsp;typS,
         java.util.List&lt;java.lang.String&gt;&nbsp;symList)</code>
<div class="block">Add LogHyp (Logical Hypothesis) to Logical System.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/LogHyp.html" title="class in mmj.lang">LogHyp</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#addLogHypForTheoremLoader(int, java.lang.String, java.lang.String, java.util.List)">addLogHypForTheoremLoader</a></strong>(int&nbsp;seq,
                         java.lang.String&nbsp;labelS,
                         java.lang.String&nbsp;typS,
                         java.util.List&lt;java.lang.String&gt;&nbsp;symList)</code>
<div class="block">Add LogHyp (Logical Hypothesis) to Logical System.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#addNewChapter(java.lang.String)">addNewChapter</a></strong>(java.lang.String&nbsp;chapterTitle)</code>
<div class="block">Add new BookManager Chapter.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#addNewSection(java.lang.String)">addNewSection</a></strong>(java.lang.String&nbsp;sectionTitle)</code>
<div class="block">Add new BookManager Section.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#addTheorem(java.lang.String, java.lang.String, java.util.List, java.util.List, mmj.mmio.BlockList, mmj.lang.Messages)">addTheorem</a></strong>(java.lang.String&nbsp;labelS,
          java.lang.String&nbsp;typS,
          java.util.List&lt;java.lang.String&gt;&nbsp;symList,
          java.util.List&lt;java.lang.String&gt;&nbsp;proofList,
          <a href="../../mmj/mmio/BlockList.html" title="class in mmj.mmio">BlockList</a>&nbsp;proofBlockList,
          <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages)</code>
<div class="block">Add Theorem to Logical System.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#addTheorem(java.lang.String, java.lang.String, java.util.List, java.util.List, mmj.lang.Messages)">addTheorem</a></strong>(java.lang.String&nbsp;labelS,
          java.lang.String&nbsp;typS,
          java.util.List&lt;java.lang.String&gt;&nbsp;symList,
          java.util.List&lt;java.lang.String&gt;&nbsp;proofList,
          <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages)</code>
<div class="block">Add Theorem to Logical System.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#addTheoremForTheoremLoader(int, java.lang.String, java.lang.String, java.util.List, java.util.List)">addTheoremForTheoremLoader</a></strong>(int&nbsp;seq,
                          java.lang.String&nbsp;labelS,
                          java.lang.String&nbsp;typS,
                          java.util.List&lt;java.lang.String&gt;&nbsp;symList,
                          java.util.List&lt;java.lang.String&gt;&nbsp;proofList)</code>
<div class="block">Add Theorem to Logical System for TheoremLoader.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#addVar(java.lang.String)">addVar</a></strong>(java.lang.String&nbsp;id)</code>
<div class="block">Add Var to Logical System.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/VarHyp.html" title="class in mmj.lang">VarHyp</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#addVarHyp(java.lang.String, java.lang.String, java.lang.String)">addVarHyp</a></strong>(java.lang.String&nbsp;labelS,
         java.lang.String&nbsp;typS,
         java.lang.String&nbsp;varS)</code>
<div class="block">Add VarHyp to Logical System.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#beginScope()">beginScope</a></strong>()</code>
<div class="block">Begin a new (nested) scope level for the Logical System.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#cacheTypesettingCommentForGMFF(java.lang.String)">cacheTypesettingCommentForGMFF</a></strong>(java.lang.String&nbsp;comment)</code>
<div class="block">Cache Metamath comment containing typesetting definitions for use by
 GMFF.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#clearTheoremLoaderCommitListenerList()">clearTheoremLoaderCommitListenerList</a></strong>()</code>
<div class="block">Empties the TheoremLoaderCommitListener list.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#endScope()">endScope</a></strong>()</code>
<div class="block">Ends a (nested) scope level for the Logical System.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#finalizeEOF(mmj.lang.Messages, boolean)">finalizeEOF</a></strong>(<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
           boolean&nbsp;prematureEOF)</code>
<div class="block">EOF processing for Logical System after file loaded.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/BookManager.html" title="class in mmj.lang">BookManager</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#getBookManager()">getBookManager</a></strong>()</code>
<div class="block">Returns the Book Manager.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/ScopeDef.html" title="class in mmj.lang">ScopeDef</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#getCurrScopeDef()">getCurrScopeDef</a></strong>()</code>
<div class="block">Get current ScopeDef object in use.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/gmff/GMFFManager.html" title="class in mmj.gmff">GMFFManager</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#getGMFFManager()">getGMFFManager</a></strong>()</code>
<div class="block">Returns the GMFF Manager.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#getLogicStmtTypeParm()">getLogicStmtTypeParm</a></strong>()</code>
<div class="block">Returns the logic stmt type code string value.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/ProofCompression.html" title="class in mmj.lang">ProofCompression</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#getProofCompression()">getProofCompression</a></strong>()</code>
<div class="block">Returns an instance of ProofCompression.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/ProofVerifier.html" title="interface in mmj.lang">ProofVerifier</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#getProofVerifier()">getProofVerifier</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#getProvableLogicStmtTypeParm()">getProvableLogicStmtTypeParm</a></strong>()</code>
<div class="block">Returns the provable logic stmt type code string value.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>java.util.List&lt;<a href="../../mmj/lang/ScopeDef.html" title="class in mmj.lang">ScopeDef</a>&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#getScopeDefList()">getScopeDefList</a></strong>()</code>
<div class="block">Get LogicalSystem scopeDefList</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#getScopeLvl()">getScopeLvl</a></strong>()</code>
<div class="block">Get current scope level.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/SeqAssigner.html" title="class in mmj.lang">SeqAssigner</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#getSeqAssigner()">getSeqAssigner</a></strong>()</code>
<div class="block">Returns the SeqAssigner.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#getStmtTbl()">getStmtTbl</a></strong>()</code>
<div class="block">Returns the current stmtTbl, a Map containing all <code>Hyp</code>s and
 <code>Assrt</code>s.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#getSymTbl()">getSymTbl</a></strong>()</code>
<div class="block">Returns the current symTbl, a Map containing all <code>Cnst</code>s and
 <code>Var</code>s.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/SyntaxVerifier.html" title="interface in mmj.lang">SyntaxVerifier</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#getSyntaxVerifier()">getSyntaxVerifier</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#isBookManagerEnabled()">isBookManagerEnabled</a></strong>()</code>
<div class="block">Is BookManager enabled?</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#removeTheoremLoaderCommitListener(mmj.tl.TheoremLoaderCommitListener)">removeTheoremLoaderCommitListener</a></strong>(<a href="../../mmj/tl/TheoremLoaderCommitListener.html" title="interface in mmj.tl">TheoremLoaderCommitListener</a>&nbsp;t)</code>
<div class="block">Removes a TheoremLoaderCommitListener from the
 TheoremLoaderCommitListener list if the instance is in the list.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#setProofCompression(mmj.lang.ProofCompression)">setProofCompression</a></strong>(<a href="../../mmj/lang/ProofCompression.html" title="class in mmj.lang">ProofCompression</a>&nbsp;proofCompression)</code>
<div class="block">Sets the reference to the local ProofCompression instance.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/ProofVerifier.html" title="interface in mmj.lang">ProofVerifier</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#setProofVerifier(mmj.lang.ProofVerifier)">setProofVerifier</a></strong>(<a href="../../mmj/lang/ProofVerifier.html" title="interface in mmj.lang">ProofVerifier</a>&nbsp;newProofVerifier)</code>
<div class="block">Sets the current ProofVerifier.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/SyntaxVerifier.html" title="interface in mmj.lang">SyntaxVerifier</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#setSyntaxVerifier(mmj.lang.SyntaxVerifier)">setSyntaxVerifier</a></strong>(<a href="../../mmj/lang/SyntaxVerifier.html" title="interface in mmj.lang">SyntaxVerifier</a>&nbsp;newSyntaxVerifier)</code>
<div class="block">Sets the current SyntaxVerifier.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#theoremLoaderCommit(mmj.tl.MMTTheoremSet)">theoremLoaderCommit</a></strong>(<a href="../../mmj/tl/MMTTheoremSet.html" title="class in mmj.tl">MMTTheoremSet</a>&nbsp;mmtTheoremSet)</code>
<div class="block">Finalizes any changes made to the mmj2 state by TheoremLoader for a
 mmtTheoremSet set of updates.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#theoremLoaderRollback(mmj.tl.MMTTheoremSet, java.lang.String, mmj.lang.Messages, boolean)">theoremLoaderRollback</a></strong>(<a href="../../mmj/tl/MMTTheoremSet.html" title="class in mmj.tl">MMTTheoremSet</a>&nbsp;mmtTheoremSet,
                     java.lang.String&nbsp;errorMessage,
                     <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
                     boolean&nbsp;auditMessages)</code>
<div class="block">Reverses any changes made to the mmj2 state by TheoremLoader for a
 mmtTheoremSet set of updates.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#verifyAllExprRPNAsProofs(mmj.lang.Messages)">verifyAllExprRPNAsProofs</a></strong>(<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages)</code>
<div class="block">Double-checks the results of <code>verifyAllSyntax</code> by feeding the
 output <code>exprRPN</code>'s through the ProofVerifier.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#verifyAllSyntax(mmj.lang.Messages)">verifyAllSyntax</a></strong>(<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages)</code>
<div class="block">Does Syntactical Analysis of the grammar and all statements in the
 LogicalSystem.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/LogicalSystem.html#verifyProofs(mmj.lang.Messages)">verifyProofs</a></strong>(<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages)</code>
<div class="block">Verifies every theorem's proof according to Metamath.pdf specifications.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="LogicalSystem(java.lang.String, java.lang.String, mmj.gmff.GMFFManager, mmj.lang.BookManager, mmj.lang.SeqAssigner, int, int, mmj.lang.ProofVerifier, mmj.lang.SyntaxVerifier)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>LogicalSystem</h4>
<pre>public&nbsp;LogicalSystem(java.lang.String&nbsp;provableLogicStmtTypeParm,
             java.lang.String&nbsp;logicStmtTypeParm,
             <a href="../../mmj/gmff/GMFFManager.html" title="class in mmj.gmff">GMFFManager</a>&nbsp;gmffManager,
             <a href="../../mmj/lang/BookManager.html" title="class in mmj.lang">BookManager</a>&nbsp;bookManager,
             <a href="../../mmj/lang/SeqAssigner.html" title="class in mmj.lang">SeqAssigner</a>&nbsp;seqAssigner,
             int&nbsp;symTblInitialSize,
             int&nbsp;stmtTblInitialSize,
             <a href="../../mmj/lang/ProofVerifier.html" title="interface in mmj.lang">ProofVerifier</a>&nbsp;proofVerifier,
             <a href="../../mmj/lang/SyntaxVerifier.html" title="interface in mmj.lang">SyntaxVerifier</a>&nbsp;syntaxVerifier)</pre>
<div class="block">Construct with full set of parameters.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>provableLogicStmtTypeParm</code> - Type Code String of provable statements.
            Defaults to "|-".</dd><dd><code>logicStmtTypeParm</code> - Type Code String value of logic expressions.
            Defaults to "wff".</dd><dd><code>gmffManager</code> - used for Graphics Mode Formula Formatting in Proof
            Assistant but loaded with $t typesetting info by Systemizer.</dd><dd><code>bookManager</code> - optional, used for tracking MObjs by Chapter and
            Section number.</dd><dd><code>seqAssigner</code> - used to generate sequence numbers for MObjs</dd><dd><code>symTblInitialSize</code> - should equal number of constant and variables,
            times 1.33 plus a fudge factor. If set too small the system
            will automatically increase, but at the expense of
            reallocating and copying. BUT, if the input value is less than
            10, the program assumes a programming error exists and throws
            an IllegalArgumentException. A suggested default value is
            provided in LangConstants.java.</dd><dd><code>stmtTblInitialSize</code> - should equal number of variable and logical
            hypotheses plus the number of axioms and theorems, times 1.33
            plus a fudge factor. If set too small the system will
            automatically increase, but at the expense of reallocating and
            copying. BUT, if the input value is less than 100, the program
            assumes a programming error exists and throws an
            IllegalArgumentException. A suggested default value is
            provided in LangConstants.java.</dd><dd><code>proofVerifier</code> - ProofVerifier interface object. Leave null if
            automatic proof verification not desired.</dd><dd><code>syntaxVerifier</code> - SyntaxVerifier interface object. Leave null if
            automatic loading of ExprRPN's is not desired.</dd></dl>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="addCnst(java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>addCnst</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&nbsp;addCnst(java.lang.String&nbsp;id)
             throws <a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></pre>
<div class="block">Add Cnst to Logical System.
 <p>
 1) validates constant:
 <p>
 <ul>
 <li>declaration allowed only at global scope level
 <li>not a dup of any other constant or variable
 </ul>
 <p>
 2)adds to symTbl table
 <p>
 3)return the constant object that now exists in the symbol table (this is
 done for consistency with the other addXXX methods -- we want everyone to
 use the only objects that exist in LogicalSystem... otherwise, CHAOS
 would occur!</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/SystemLoader.html#addCnst(java.lang.String)">addCnst</a></code>&nbsp;in interface&nbsp;<code><a href="../../mmj/lang/SystemLoader.html" title="interface in mmj.lang">SystemLoader</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>id</code> - Constant's symbol string to be added to the Logical System.</dd>
<dt><span class="strong">Returns:</span></dt><dd>Cnst added to LogicalSystem.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></code> - if duplicate symbol, etc.</dd></dl>
</li>
</ul>
<a name="addVar(java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>addVar</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>&nbsp;addVar(java.lang.String&nbsp;id)
           throws <a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></pre>
<div class="block">Add Var to Logical System.
 <p>
 1) validates variable:
 <ul>
 <li>must not be redeclared unless currently inactive
 <li>not a dup of any other constant or variable
 </ul>
 <p>
 2) add to symTbl table; if already there but inactive, mark it active.
 <p>
 3) get current ScopeDef array list item, (if any) and add the new var to
 the scope array list of Var's.
 <p>
 4) return the variable object that now exists in the symbol table (a key
 step so that everyone is using the same object!!!)</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/SystemLoader.html#addVar(java.lang.String)">addVar</a></code>&nbsp;in interface&nbsp;<code><a href="../../mmj/lang/SystemLoader.html" title="interface in mmj.lang">SystemLoader</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>id</code> - Var's symbol string to be added to the Logical System.</dd>
<dt><span class="strong">Returns:</span></dt><dd>Var added to LogicalSystem.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></code> - if duplicate symbol, etc.</dd></dl>
</li>
</ul>
<a name="addVarHyp(java.lang.String, java.lang.String, java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>addVarHyp</h4>
<pre>public&nbsp;<a href="../../mmj/lang/VarHyp.html" title="class in mmj.lang">VarHyp</a>&nbsp;addVarHyp(java.lang.String&nbsp;labelS,
               java.lang.String&nbsp;typS,
               java.lang.String&nbsp;varS)
                 throws <a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></pre>
<div class="block">Add VarHyp to Logical System.
 <p>
 1)Validates VarHyp label:
 <p>
 <ul>
 --must not already exist (label must be unique.)
 </ul>
 <p>
 2)Validates VarHyp typ and var:
 <p>
 <ul>
 --must exist in symTbl as active Cnst and Var, respectively. --marks the
 var as "active" and the typ as a variable type.
 </ul>
 <p>
 3)Manufacture an active VarHyp, complete with sequence number
 <p>
 4)Add the new variable hypothesis to the statement table.
 <p>
 5) get current ScopeDef array list item, (if any) and add the new VarHyp
 to the scope array list of VarHyp's
 <p>
 6) return the VarHyp object that now exists in the statement table.</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/SystemLoader.html#addVarHyp(java.lang.String, java.lang.String, java.lang.String)">addVarHyp</a></code>&nbsp;in interface&nbsp;<code><a href="../../mmj/lang/SystemLoader.html" title="interface in mmj.lang">SystemLoader</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>labelS</code> - String label of variable hypothesis</dd><dd><code>typS</code> - String Metamath constant character (type code)</dd><dd><code>varS</code> - String Metamath variable character</dd>
<dt><span class="strong">Returns:</span></dt><dd>VarHyp added to LogicalSystem.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></code> - if duplicate symbol, etc. (see
             <code>mmj.lang.LangConstants.java</code>)</dd></dl>
</li>
</ul>
<a name="addDjVars(java.lang.String, java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>addDjVars</h4>
<pre>public&nbsp;<a href="../../mmj/lang/DjVars.html" title="class in mmj.lang">DjVars</a>&nbsp;addDjVars(java.lang.String&nbsp;djVar1S,
               java.lang.String&nbsp;djVar2S)
                 throws <a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></pre>
<div class="block">Add DjVars (Disjoint Variables Restriction) to Logical System.
 <p>
 1) validates disjoint variables:
 <p>
 <ul>
 <li>must be active in scope
 <li>not duplicates of each other
 </ul>
 <p>
 2) construct DjVars element (swapping the items if necessary to ensure
 varLo < varHi.--see constructor).
 <p>
 3) get current ScopeDef array list item
 <p>
 4) add the DjVars elment to the scope list of DjVars, but only if the
 pair of variables is not already there (we cannot use "==" in this case
 because DjVars are not maintained as "unique" in the same way as Sym's
 and Stmt's.)</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/SystemLoader.html#addDjVars(java.lang.String, java.lang.String)">addDjVars</a></code>&nbsp;in interface&nbsp;<code><a href="../../mmj/lang/SystemLoader.html" title="interface in mmj.lang">SystemLoader</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>djVar1S</code> - disjoint variable symbol string 1</dd><dd><code>djVar2S</code> - disjoint variable symbol string 2</dd>
<dt><span class="strong">Returns:</span></dt><dd>DjVars (pair) added to LogicalSystem.within the current scope,
         *or* the existing DjVars object in the current scope.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></code> - if duplicate vars, etc. (see
             <code>mmj.lang.LangConstants.java</code>)</dd></dl>
</li>
</ul>
<a name="addLogHyp(java.lang.String, java.lang.String, java.util.List)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>addLogHyp</h4>
<pre>public&nbsp;<a href="../../mmj/lang/LogHyp.html" title="class in mmj.lang">LogHyp</a>&nbsp;addLogHyp(java.lang.String&nbsp;labelS,
               java.lang.String&nbsp;typS,
               java.util.List&lt;java.lang.String&gt;&nbsp;symList)
                 throws <a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></pre>
<div class="block">Add LogHyp (Logical Hypothesis) to Logical System.
 <p>
 Basically a clone of <code>addAxiom</code> below, except that:
 <p>
 <ul>
 <li>there is no Frame for a logical hypothesis
 <li><code>LogHyp is a <code>Hyp</code>, not an
         <code>Assrt</code> and has
         attribute <code>"VarHyp[] varHypArray</code>.
 </ul>
 <p>
 Required processing:
 <p>
 1) validates input label, type and expression symbols, and in the process
 obtaining references to their existing definitions in LogicalSystem:
 <p>
 <ul>
 <li>must be active in scope
 <li>not be a duplicate
 <li>active VarHyp must exist for each Var.
 </ul>
 <p>
 2) construct the LogHyp object
 <p>
 3) add it to the stmtTbl and to the existing scope.
 <p>
 4) return it to the caller</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/SystemLoader.html#addLogHyp(java.lang.String, java.lang.String, java.util.List)">addLogHyp</a></code>&nbsp;in interface&nbsp;<code><a href="../../mmj/lang/SystemLoader.html" title="interface in mmj.lang">SystemLoader</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>labelS</code> - logical hypothesis label string</dd><dd><code>typS</code> - logical hypothesis type code (symbol) string</dd><dd><code>symList</code> - list containing expression symbol strings (zero or more
            symbols).</dd>
<dt><span class="strong">Returns:</span></dt><dd>LogHyp newly constructed LogHyp added to LogicalSystem.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></code> - if duplicate label, undefined vars, etc.</dd></dl>
</li>
</ul>
<a name="addLogHypForTheoremLoader(int, java.lang.String, java.lang.String, java.util.List)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>addLogHypForTheoremLoader</h4>
<pre>public&nbsp;<a href="../../mmj/lang/LogHyp.html" title="class in mmj.lang">LogHyp</a>&nbsp;addLogHypForTheoremLoader(int&nbsp;seq,
                               java.lang.String&nbsp;labelS,
                               java.lang.String&nbsp;typS,
                               java.util.List&lt;java.lang.String&gt;&nbsp;symList)
                                 throws <a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></pre>
<div class="block">Add LogHyp (Logical Hypothesis) to Logical System. for TheoremLoader.
 <p>
 The main difference from the regular addLogHyp is that the BookManager is
 not called.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>seq</code> - preassigned MObj seq number</dd><dd><code>labelS</code> - logical hypothesis label string</dd><dd><code>typS</code> - logical hypothesis type code (symbol) string</dd><dd><code>symList</code> - list containing expression symbol strings (zero or more
            symbols).</dd>
<dt><span class="strong">Returns:</span></dt><dd>LogHyp newly constructed LogHyp added to LogicalSystem.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></code> - if duplicate label, undefined vars, etc.</dd></dl>
</li>
</ul>
<a name="addAxiom(java.lang.String, java.lang.String, java.util.List)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>addAxiom</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Axiom.html" title="class in mmj.lang">Axiom</a>&nbsp;addAxiom(java.lang.String&nbsp;labelS,
             java.lang.String&nbsp;typS,
             java.util.List&lt;java.lang.String&gt;&nbsp;symList)
               throws <a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></pre>
<div class="block">Add Axiom to Logical System.
 <p>
 1) validates input label, type and expression symbols, and in the process
 obtaining references to their existing definitions in LogicalSystem:
 <p>
 <ul>
 <li>not a duplicate
 <li>active VarHyp must exist for each Var.
 </ul>
 <p>
 2) Build the MetaMath "Frame" for the Axiom (see ScopeFrame)
 <p>
 3) construct the Axiom object
 <p>
 4) add it to the stmtTbl
 <p>
 5) return it to the caller</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/SystemLoader.html#addAxiom(java.lang.String, java.lang.String, java.util.List)">addAxiom</a></code>&nbsp;in interface&nbsp;<code><a href="../../mmj/lang/SystemLoader.html" title="interface in mmj.lang">SystemLoader</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>labelS</code> - axiom label string</dd><dd><code>typS</code> - axiom type code (symbol) string</dd><dd><code>symList</code> - list containing axiom expression symbol strings (zero or
            more symbols).</dd>
<dt><span class="strong">Returns:</span></dt><dd>Axiom newly constructed Axiom added to LogicalSystem.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></code> - if duplicate label, undefined vars, etc.</dd></dl>
</li>
</ul>
<a name="addTheorem(java.lang.String, java.lang.String, java.util.List, java.util.List, mmj.lang.Messages)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>addTheorem</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&nbsp;addTheorem(java.lang.String&nbsp;labelS,
                 java.lang.String&nbsp;typS,
                 java.util.List&lt;java.lang.String&gt;&nbsp;symList,
                 java.util.List&lt;java.lang.String&gt;&nbsp;proofList,
                 <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages)
                   throws <a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></pre>
<div class="block">Add Theorem to Logical System.
 <p>
 addTheorem is basically a clone of addAxiom except that it builds an
 "extended" Frame containing "optional" hypotheses and disjoint variable
 restriction information. And it validates the input proof list then
 stores it with the new Theorem object.
 <p>
 1) validates input label, type and expression symbols, and in the process
 obtaining references to their existing definitions in LogicalSystem:
 <ul>
 <li>must be active in scope
 <li>not a duplicate
 <li>active VarHyp must exist for each Var.
 </ul>
 <p>
 2) Build the MetaMath Extended Frame for the Theorem (consists here in
 mmj of MandFrame + OptFrame).
 <p>
 3) Validates proof steps
 <p>
 4) Construct Theorem object
 <p>
 5) add it to the stmtTbl
 <p>
 6) return it to the caller</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/SystemLoader.html#addTheorem(java.lang.String, java.lang.String, java.util.List, java.util.List, mmj.lang.Messages)">addTheorem</a></code>&nbsp;in interface&nbsp;<code><a href="../../mmj/lang/SystemLoader.html" title="interface in mmj.lang">SystemLoader</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>labelS</code> - axiom label string</dd><dd><code>typS</code> - axiom type code (symbol) string</dd><dd><code>symList</code> - list containing axiom expression symbol strings (zero or
            more symbols).</dd><dd><code>proofList</code> - list containing proof step symbol strings (1 or more
            symbols -- which may be "?" if a step is unknown).</dd><dd><code>messages</code> - for error reporting</dd>
<dt><span class="strong">Returns:</span></dt><dd>Theorem newly constructed Theorem added to LogicalSystem.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></code> - if duplicate label, undefined vars, etc.</dd></dl>
</li>
</ul>
<a name="addTheoremForTheoremLoader(int, java.lang.String, java.lang.String, java.util.List, java.util.List)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>addTheoremForTheoremLoader</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&nbsp;addTheoremForTheoremLoader(int&nbsp;seq,
                                 java.lang.String&nbsp;labelS,
                                 java.lang.String&nbsp;typS,
                                 java.util.List&lt;java.lang.String&gt;&nbsp;symList,
                                 java.util.List&lt;java.lang.String&gt;&nbsp;proofList)
                                   throws <a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></pre>
<div class="block">Add Theorem to Logical System for TheoremLoader.
 <p>
 Main difference of regular addTheorem is that it does not call
 BookManager.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>seq</code> - preassigned MObj seq number</dd><dd><code>labelS</code> - axiom label string</dd><dd><code>typS</code> - axiom type code (symbol) string</dd><dd><code>symList</code> - list containing axiom expression symbol strings (zero or
            more symbols).</dd><dd><code>proofList</code> - list containing proof step symbol strings (1 or more
            symbols -- which may be "?" if a step is unknown).</dd>
<dt><span class="strong">Returns:</span></dt><dd>Theorem newly constructed Theorem added to LogicalSystem.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></code> - if duplicate label, undefined vars, etc.</dd></dl>
</li>
</ul>
<a name="addTheorem(java.lang.String, java.lang.String, java.util.List, java.util.List, mmj.mmio.BlockList, mmj.lang.Messages)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>addTheorem</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&nbsp;addTheorem(java.lang.String&nbsp;labelS,
                 java.lang.String&nbsp;typS,
                 java.util.List&lt;java.lang.String&gt;&nbsp;symList,
                 java.util.List&lt;java.lang.String&gt;&nbsp;proofList,
                 <a href="../../mmj/mmio/BlockList.html" title="class in mmj.mmio">BlockList</a>&nbsp;proofBlockList,
                 <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages)
                   throws <a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></pre>
<div class="block">Add Theorem to Logical System.
 <p>
 addTheorem is basically a clone of addAxiom except that it builds an
 "extended" Frame containing "optional" hypotheses and disjoint variable
 restriction information. And it validates the input proof list then
 stores it with the new Theorem object.
 <p>
 This variant is invoked when the input contains a compressed proof.</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/SystemLoader.html#addTheorem(java.lang.String, java.lang.String, java.util.List, java.util.List, mmj.mmio.BlockList, mmj.lang.Messages)">addTheorem</a></code>&nbsp;in interface&nbsp;<code><a href="../../mmj/lang/SystemLoader.html" title="interface in mmj.lang">SystemLoader</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>labelS</code> - axiom label string</dd><dd><code>typS</code> - axiom type code (symbol) string</dd><dd><code>symList</code> - list containing axiom expression symbol strings (zero or
            more symbols).</dd><dd><code>proofList</code> - list containing the contents of the parenthesized
            portion of a compressed proof (does not include the
            parentheses)</dd><dd><code>proofBlockList</code> - list containing one or more blocks of compressed
            proof symbols.</dd><dd><code>messages</code> - for error reporting</dd>
<dt><span class="strong">Returns:</span></dt><dd>Theorem newly constructed Theorem added to LogicalSystem.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></code> - if duplicate label, undefined vars, etc.</dd></dl>
</li>
</ul>
<a name="beginScope()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>beginScope</h4>
<pre>public&nbsp;void&nbsp;beginScope()</pre>
<div class="block">Begin a new (nested) scope level for the Logical System.
 <p>
 Adds a new ScopeDef item to the "stack" and increments the level number
 by 1 (all of the hard work is in endScope()!)
 <p>
 Note: *global* scope has level number = 0.</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/SystemLoader.html#beginScope()">beginScope</a></code>&nbsp;in interface&nbsp;<code><a href="../../mmj/lang/SystemLoader.html" title="interface in mmj.lang">SystemLoader</a></code></dd>
<dt><span class="strong">See Also:</span></dt><dd><a href="../../mmj/lang/ScopeDef.html" title="class in mmj.lang"><code>ScopeDef</code></a></dd></dl>
</li>
</ul>
<a name="endScope()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>endScope</h4>
<pre>public&nbsp;void&nbsp;endScope()
              throws <a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></pre>
<div class="block">Ends a (nested) scope level for the Logical System.
 <p>
 Processing:
 <p>
 1) if scope level = 0 (global), raise LangException.
 <p>
 otherwise,
 <p>
 2)
 <ol>
 <li>go through items in ScopeDef for the current level (Var, VarHyp, and
 LogVar) and mark them inactive (not forgetting the Var attribute
 "activeVarHyp" when deactivating the corresponding VarHyp.)
 <li>remove the scope level from the stack
 <li>decrement current scope level number
 </ol></div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/SystemLoader.html#endScope()">endScope</a></code>&nbsp;in interface&nbsp;<code><a href="../../mmj/lang/SystemLoader.html" title="interface in mmj.lang">SystemLoader</a></code></dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></code> - if scope is already at the global scope level.</dd><dt><span class="strong">See Also:</span></dt><dd><a href="../../mmj/lang/ScopeDef.html" title="class in mmj.lang"><code>ScopeDef</code></a></dd></dl>
</li>
</ul>
<a name="finalizeEOF(mmj.lang.Messages, boolean)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>finalizeEOF</h4>
<pre>public&nbsp;void&nbsp;finalizeEOF(<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
               boolean&nbsp;prematureEOF)
                 throws <a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></pre>
<div class="block">EOF processing for Logical System after file loaded.
 <p>
 Called at end of file to verify that there was an End Scope statement for
 each Begin Scope. At the time this routine is called, the ScopeDef list
 should contain just one entry, the "global" scope level (which is, by
 definition, level 0.)</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/SystemLoader.html#finalizeEOF(mmj.lang.Messages, boolean)">finalizeEOF</a></code>&nbsp;in interface&nbsp;<code><a href="../../mmj/lang/SystemLoader.html" title="interface in mmj.lang">SystemLoader</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>messages</code> - Messages object to error reporting.</dd><dd><code>prematureEOF</code> - signals LoadLimit requested by user has been reached,
            so stop loading even if in the middle of a scope level.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></code> - if scope is NOT at the global scope level UNLESS
             premature EOF signalled. (see
             <code>mmj.lang.LangConstants.java</code>)</dd></dl>
</li>
</ul>
<a name="verifyAllSyntax(mmj.lang.Messages)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>verifyAllSyntax</h4>
<pre>public&nbsp;void&nbsp;verifyAllSyntax(<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages)
                     throws <a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></pre>
<div class="block">Does Syntactical Analysis of the grammar and all statements in the
 LogicalSystem.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>messages</code> - <code>Messages</code> object for reporting errors.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></code> - if an error occurred</dd></dl>
</li>
</ul>
<a name="verifyProofs(mmj.lang.Messages)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>verifyProofs</h4>
<pre>public&nbsp;void&nbsp;verifyProofs(<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages)
                  throws <a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></pre>
<div class="block">Verifies every theorem's proof according to Metamath.pdf specifications.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>messages</code> - <code>Messages</code> object for reporting errors.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></code> - if an error occurred</dd></dl>
</li>
</ul>
<a name="verifyAllExprRPNAsProofs(mmj.lang.Messages)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>verifyAllExprRPNAsProofs</h4>
<pre>public&nbsp;void&nbsp;verifyAllExprRPNAsProofs(<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages)
                              throws <a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></pre>
<div class="block">Double-checks the results of <code>verifyAllSyntax</code> by feeding the
 output <code>exprRPN</code>'s through the ProofVerifier.
 <p>
 Based on the fact that the output of the grammatical parser is a *proof*
 that a statement's formula can be generated using the grammatical parse
 tree -- which is stored in LogicalSystem in Reverse Polish Notation, like
 proofs.
 <p>
 Should not be necessary in normal use, but is very helpful for testing.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>messages</code> - <code>Messages</code> object for reporting errors.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></code> - if an error occurred</dd></dl>
</li>
</ul>
<a name="getScopeDefList()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getScopeDefList</h4>
<pre>public&nbsp;java.util.List&lt;<a href="../../mmj/lang/ScopeDef.html" title="class in mmj.lang">ScopeDef</a>&gt;&nbsp;getScopeDefList()</pre>
<div class="block">Get LogicalSystem scopeDefList
 <p>
 scopeDefList is an List of ScopeDef objects where element 0 is global
 scope, element 1 is scope level 1, etc. At the end of LoadFile the
 scopeDefList should contain only 1 element -- the global ScopeDef.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>List of ScopeDef objects.</dd></dl>
</li>
</ul>
<a name="getCurrScopeDef()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getCurrScopeDef</h4>
<pre>public&nbsp;<a href="../../mmj/lang/ScopeDef.html" title="class in mmj.lang">ScopeDef</a>&nbsp;getCurrScopeDef()</pre>
<div class="block">Get current ScopeDef object in use.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>current ScopeDef object in use.</dd></dl>
</li>
</ul>
<a name="getScopeLvl()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getScopeLvl</h4>
<pre>public&nbsp;int&nbsp;getScopeLvl()</pre>
<div class="block">Get current scope level.
 <p>
 Level 0 is global scope, 1 is level 1, etc.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>current scope level.</dd></dl>
</li>
</ul>
<a name="getProofVerifier()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getProofVerifier</h4>
<pre>public&nbsp;<a href="../../mmj/lang/ProofVerifier.html" title="interface in mmj.lang">ProofVerifier</a>&nbsp;getProofVerifier()</pre>
<dl><dt><span class="strong">Returns:</span></dt><dd>the current ProofVerifier.</dd></dl>
</li>
</ul>
<a name="setProofVerifier(mmj.lang.ProofVerifier)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>setProofVerifier</h4>
<pre>public&nbsp;<a href="../../mmj/lang/ProofVerifier.html" title="interface in mmj.lang">ProofVerifier</a>&nbsp;setProofVerifier(<a href="../../mmj/lang/ProofVerifier.html" title="interface in mmj.lang">ProofVerifier</a>&nbsp;newProofVerifier)</pre>
<div class="block">Sets the current ProofVerifier.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>newProofVerifier</code> - a ProofVerifier or null is ok.</dd>
<dt><span class="strong">Returns:</span></dt><dd>the old ProofVerifier in use in LogicalSystem.</dd></dl>
</li>
</ul>
<a name="getSyntaxVerifier()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getSyntaxVerifier</h4>
<pre>public&nbsp;<a href="../../mmj/lang/SyntaxVerifier.html" title="interface in mmj.lang">SyntaxVerifier</a>&nbsp;getSyntaxVerifier()</pre>
<dl><dt><span class="strong">Returns:</span></dt><dd>the current SyntaxVerifier.</dd></dl>
</li>
</ul>
<a name="setSyntaxVerifier(mmj.lang.SyntaxVerifier)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>setSyntaxVerifier</h4>
<pre>public&nbsp;<a href="../../mmj/lang/SyntaxVerifier.html" title="interface in mmj.lang">SyntaxVerifier</a>&nbsp;setSyntaxVerifier(<a href="../../mmj/lang/SyntaxVerifier.html" title="interface in mmj.lang">SyntaxVerifier</a>&nbsp;newSyntaxVerifier)</pre>
<div class="block">Sets the current SyntaxVerifier.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>newSyntaxVerifier</code> - a SyntaxVerifier or null is ok.</dd>
<dt><span class="strong">Returns:</span></dt><dd>the old SyntaxVerifier in use in LogicalSystem.</dd></dl>
</li>
</ul>
<a name="getSymTbl()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getSymTbl</h4>
<pre>public&nbsp;java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;getSymTbl()</pre>
<div class="block">Returns the current symTbl, a Map containing all <code>Cnst</code>s and
 <code>Var</code>s.
 <p>
 Note: in theory, symTbl is an excellent candidate for being a real class.
 There are numerous operations involving it, and more possibilities.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>symTbl map of all <code>Cnst</code>s and <code>Var</code>s.</dd></dl>
</li>
</ul>
<a name="getStmtTbl()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getStmtTbl</h4>
<pre>public&nbsp;java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;getStmtTbl()</pre>
<div class="block">Returns the current stmtTbl, a Map containing all <code>Hyp</code>s and
 <code>Assrt</code>s.
 <p>
 Note: in theory, stmtTbl is an excellent candidate for being a real
 class. There are numerous operations involving it, and more
 possibilities.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>stmtTbl map of all <code>Hyp</code>s and <code>Assrt</code>s.</dd></dl>
</li>
</ul>
<a name="getProofCompression()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getProofCompression</h4>
<pre>public&nbsp;<a href="../../mmj/lang/ProofCompression.html" title="class in mmj.lang">ProofCompression</a>&nbsp;getProofCompression()</pre>
<div class="block">Returns an instance of ProofCompression.
 <p>
 Reuses the existing ProofCompression instance if present, otherwise
 constructs one.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>ProofCompression instance.</dd></dl>
</li>
</ul>
<a name="setProofCompression(mmj.lang.ProofCompression)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>setProofCompression</h4>
<pre>public&nbsp;void&nbsp;setProofCompression(<a href="../../mmj/lang/ProofCompression.html" title="class in mmj.lang">ProofCompression</a>&nbsp;proofCompression)</pre>
<div class="block">Sets the reference to the local ProofCompression instance.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>proofCompression</code> - instance or null.</dd></dl>
</li>
</ul>
<a name="getProvableLogicStmtTypeParm()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getProvableLogicStmtTypeParm</h4>
<pre>public&nbsp;java.lang.String&nbsp;getProvableLogicStmtTypeParm()</pre>
<div class="block">Returns the provable logic stmt type code string value.
 <p>
 (Default value is "|-", fyi.)</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>provableLogicStmtTypeParm.</dd></dl>
</li>
</ul>
<a name="getLogicStmtTypeParm()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getLogicStmtTypeParm</h4>
<pre>public&nbsp;java.lang.String&nbsp;getLogicStmtTypeParm()</pre>
<div class="block">Returns the logic stmt type code string value.
 <p>
 (Default value is "wff", fyi.)</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>logicStmtTypeParm.</dd></dl>
</li>
</ul>
<a name="getGMFFManager()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getGMFFManager</h4>
<pre>public&nbsp;<a href="../../mmj/gmff/GMFFManager.html" title="class in mmj.gmff">GMFFManager</a>&nbsp;getGMFFManager()</pre>
<div class="block">Returns the GMFF Manager.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>GMFF Manager in use (may not be enabled!)</dd></dl>
</li>
</ul>
<a name="cacheTypesettingCommentForGMFF(java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>cacheTypesettingCommentForGMFF</h4>
<pre>public&nbsp;void&nbsp;cacheTypesettingCommentForGMFF(java.lang.String&nbsp;comment)</pre>
<div class="block">Cache Metamath comment containing typesetting definitions for use by
 GMFF.
 <p>
 Note: comment is from mmj.mmio.SrcStmt so it does not contain the "$("
 and "$)" start/end comment id tokens which are standard to Metamath
 comments.
 <p>
 Note: per agreement with Norm, the "$t" token identifying typesetting
 definitions in a comment is the first non-whitespace token after the "$("
 in the comment.</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/SystemLoader.html#cacheTypesettingCommentForGMFF(java.lang.String)">cacheTypesettingCommentForGMFF</a></code>&nbsp;in interface&nbsp;<code><a href="../../mmj/lang/SystemLoader.html" title="interface in mmj.lang">SystemLoader</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>comment</code> - Typesetting definition comment ("$t) from Metamath file
            minus the "$(" and "$)" tokens.</dd></dl>
</li>
</ul>
<a name="getBookManager()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getBookManager</h4>
<pre>public&nbsp;<a href="../../mmj/lang/BookManager.html" title="class in mmj.lang">BookManager</a>&nbsp;getBookManager()</pre>
<div class="block">Returns the Book Manager.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>Book Manager in use (may not be enabled!)</dd></dl>
</li>
</ul>
<a name="addNewChapter(java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>addNewChapter</h4>
<pre>public&nbsp;void&nbsp;addNewChapter(java.lang.String&nbsp;chapterTitle)</pre>
<div class="block">Add new BookManager Chapter.
 <p>
 See mmj.lang.BookManager.java for more info.</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/SystemLoader.html#addNewChapter(java.lang.String)">addNewChapter</a></code>&nbsp;in interface&nbsp;<code><a href="../../mmj/lang/SystemLoader.html" title="interface in mmj.lang">SystemLoader</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>chapterTitle</code> - Title of chapter or blank or empty String.</dd></dl>
</li>
</ul>
<a name="addNewSection(java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>addNewSection</h4>
<pre>public&nbsp;void&nbsp;addNewSection(java.lang.String&nbsp;sectionTitle)</pre>
<div class="block">Add new BookManager Section.
 <p>
 See mmj.lang.BookManager.java for more info.</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/SystemLoader.html#addNewSection(java.lang.String)">addNewSection</a></code>&nbsp;in interface&nbsp;<code><a href="../../mmj/lang/SystemLoader.html" title="interface in mmj.lang">SystemLoader</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>sectionTitle</code> - Title of section or blank or empty String.</dd></dl>
</li>
</ul>
<a name="isBookManagerEnabled()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>isBookManagerEnabled</h4>
<pre>public&nbsp;boolean&nbsp;isBookManagerEnabled()</pre>
<div class="block">Is BookManager enabled?
 <p>
 If BookManager is enabled then Chapters and Sections will be stored.</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/SystemLoader.html#isBookManagerEnabled()">isBookManagerEnabled</a></code>&nbsp;in interface&nbsp;<code><a href="../../mmj/lang/SystemLoader.html" title="interface in mmj.lang">SystemLoader</a></code></dd>
<dt><span class="strong">Returns:</span></dt><dd>true if BookManager is enabled.</dd></dl>
</li>
</ul>
<a name="getSeqAssigner()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getSeqAssigner</h4>
<pre>public&nbsp;<a href="../../mmj/lang/SeqAssigner.html" title="class in mmj.lang">SeqAssigner</a>&nbsp;getSeqAssigner()</pre>
<div class="block">Returns the SeqAssigner.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>seqAssigner.</dd></dl>
</li>
</ul>
<a name="clearTheoremLoaderCommitListenerList()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>clearTheoremLoaderCommitListenerList</h4>
<pre>public&nbsp;void&nbsp;clearTheoremLoaderCommitListenerList()</pre>
<div class="block">Empties the TheoremLoaderCommitListener list.</div>
</li>
</ul>
<a name="accumTheoremLoaderCommitListener(mmj.tl.TheoremLoaderCommitListener)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>accumTheoremLoaderCommitListener</h4>
<pre>public&nbsp;void&nbsp;accumTheoremLoaderCommitListener(<a href="../../mmj/tl/TheoremLoaderCommitListener.html" title="interface in mmj.tl">TheoremLoaderCommitListener</a>&nbsp;t)</pre>
<div class="block">Adds a TheoremLoaderCommitListener to the TheoremLoaderCommitListener
 list if the instance is not already in the list.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>t</code> - TheoremLoaderCommitListener object.</dd></dl>
</li>
</ul>
<a name="removeTheoremLoaderCommitListener(mmj.tl.TheoremLoaderCommitListener)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>removeTheoremLoaderCommitListener</h4>
<pre>public&nbsp;void&nbsp;removeTheoremLoaderCommitListener(<a href="../../mmj/tl/TheoremLoaderCommitListener.html" title="interface in mmj.tl">TheoremLoaderCommitListener</a>&nbsp;t)</pre>
<div class="block">Removes a TheoremLoaderCommitListener from the
 TheoremLoaderCommitListener list if the instance is in the list.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>t</code> - TheoremLoaderCommitListener object.</dd></dl>
</li>
</ul>
<a name="theoremLoaderRollback(mmj.tl.MMTTheoremSet, java.lang.String, mmj.lang.Messages, boolean)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>theoremLoaderRollback</h4>
<pre>public&nbsp;void&nbsp;theoremLoaderRollback(<a href="../../mmj/tl/MMTTheoremSet.html" title="class in mmj.tl">MMTTheoremSet</a>&nbsp;mmtTheoremSet,
                         java.lang.String&nbsp;errorMessage,
                         <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
                         boolean&nbsp;auditMessages)</pre>
<div class="block">Reverses any changes made to the mmj2 state by TheoremLoader for a
 mmtTheoremSet set of updates.
 <p>
 Reverses any changes to the LogicalSystem scopeDefList.
 <p>
 Rollsback any changes to the SeqAssigner.
 <p>
 Scans the mmtTheoremSet and un-does each TheoremStmtGroup object's
 updates, if any,</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>mmtTheoremSet</code> - set of MMTTheoremStmtGroups which may or may not
            have already been updated into mmj2.</dd><dd><code>errorMessage</code> - an explanatory message about the cause of the
            rollback to be inserted into a final message if the rollback
            itself fails.</dd><dd><code>messages</code> - Messages object.</dd><dd><code>auditMessages</code> - flag indicating whether or not audit messages about
            the rollback are to be written to the Messages object.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code>java.lang.IllegalArgumentException</code> - if the rollback operation fails.</dd></dl>
</li>
</ul>
<a name="theoremLoaderCommit(mmj.tl.MMTTheoremSet)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>theoremLoaderCommit</h4>
<pre>public&nbsp;void&nbsp;theoremLoaderCommit(<a href="../../mmj/tl/MMTTheoremSet.html" title="class in mmj.tl">MMTTheoremSet</a>&nbsp;mmtTheoremSet)</pre>
<div class="block">Finalizes any changes made to the mmj2 state by TheoremLoader for a
 mmtTheoremSet set of updates.
 <p>
 Commits SeqAssigner updates.
 <p>
 Commits BookManager updates.
 <p>
 Sends commit() request to every TheoremLoaderCommitListener.
 <p></div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>mmtTheoremSet</code> - set of MMTTheoremStmtGroups which may or may not
            have already been updated into mmj2.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code>java.lang.IllegalArgumentException</code> - if the commit operation fails.</dd></dl>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/lang/LogHyp.html" title="class in mmj.lang"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/lang/LogicFormula.html" title="class in mmj.lang"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/lang/LogicalSystem.html" target="_top">Frames</a></li>
<li><a href="LogicalSystem.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
